{-# OPTIONS --profile=interactive #-}
open import Common.Prelude
open import Common.Equality

`1     = suc zero
`2     =     `1 +     `1
`4     =     `2 +     `2
`8     =     `4 +     `4
`16    =     `8 +     `8
`32    =    `16 +    `16
`64    =    `32 +    `32
`128   =    `64 +    `64
`256   =   `128 +   `128
`512   =   `256 +   `256
`1024  =   `512 +   `512
`2048  =  `1024 +  `1024
`4096  =  `2048 +  `2048
`8192  =  `4096 +  `4096
`16384 =  `8192 +  `8192
`32768 = `16384 + `16384
`65536 = `32768 + `32768

prf8 : `8 ≡ 8
prf8 = refl

prf65k : `65536 ≡ 65536
prf65k = refl
